Lean External Network Term Format

inductive tree.{l} (A : Type.{l}) : Type.{max 1 l} :=
| node  : tree_list.{l} A → tree.{l} A
| empty : tree.{l} A

with tree_list : Type.{max 1 l} :=
| nil  : tree_list.{l} A
| cons : tree.{l} A → tree_list.{l} A → tree_list.{l} A

Компилируется в такой байткод:

2 #NS 0 l       // терминалы
3 #NS 0 tree
4 #NS 0 A
1 #UP 2         // параметр вселенной
0 #ES 1         // sort терма l
2 #US 0         // следующая вселенная после 1
3 #UM 2 1       // максимум 2 и 1
1 #ES 3         // sort терма 3
2 #EP #D 4 0 1  // Пи-тип
5 #NS 3 node
6 #NS 0 a
7 #NS 0 tree_list
3 #EC 7 1
4 #EV 0
5 #EA 3 4
6 #EC 3 1
7 #EV 1
8 #EA 6 7
9 #EP #BD 6 5 8     // Пи-тип
10 #EP #BI 4 0 9    // Пи-тип
8 #NS 3 empty
11 #EA 6 4
12 #EP #BD 4 0 11   // Пи-тип
9 #NS 7 nil
13 #EP #BD 4 0 5    // Пи-тип
10 #NS 7 cons
14 #EA 3 7
15 #EV 2
16 #EA 3 15
17 #EP #BD 6 14 16
18 #EP #BD 6 11 17
19 #EP #BI 4 0 18
#BIND 1 2 2           // начало блока взаиморекурсивных типов
#IND 3 2              // первый индуктивный тип
#INTRO 5 10           // место конструктора node
#INTRO 8 12           // место конструктора empty
#IND 7 2              // второй индуктивный тип
#INTRO 9 13           // место конструктора nil
#INTRO 10 19          // место конструктора cons
#EIND

_________
[1]. https://github.com/leanprover/lean/blob/master/doc/export_format.md
[2]. https://github.com/leanprover/tc Внешний тайпчекер на Хаскеле